Let's prove the following theorem:

result of appending [4, 7] to [ ] = [ [4, 7], [ ] ]

Proof Table

#	Claim	Reason
1	result of appending `[4, 7]` to [ ] = reverse of [ `[4, 7]`, reverse of [ ] ]	result of appending `[4, 7]` to [ ] = reverse of [ `[4, 7]`, reverse of [ ] ] (Appending to a List Property)
2	reverse of [ ] = [ ]	reverse of [ ] = [ ] (do_reverse_9_0)
3	[ `[4, 7]`, reverse of [ ] ] = [ `[4, 7]`, [ ] ]	if reverse of [ ] = [ ], then [ `[4, 7]`, reverse of [ ] ] = [ `[4, 7]`, [ ] ] (Substitution)
4	reverse of [ `[4, 7]`, reverse of [ ] ] = reverse of [ `[4, 7]`, [ ] ]	if [ `[4, 7]`, reverse of [ ] ] = [ `[4, 7]`, [ ] ], then reverse of [ `[4, 7]`, reverse of [ ] ] = reverse of [ `[4, 7]`, [ ] ] (Substitution)
5	reverse of [ `[4, 7]`, [ ] ] = [ `[4, 7]`, [ ] ]	reverse of [ `[4, 7]`, [ ] ] = [ `[4, 7]`, [ ] ] (do_reverse_9_1)
6	reverse of [ `[4, 7]`, reverse of [ ] ] = [ `[4, 7]`, [ ] ]	if reverse of [ `[4, 7]`, reverse of [ ] ] = reverse of [ `[4, 7]`, [ ] ] and reverse of [ `[4, 7]`, [ ] ] = [ `[4, 7]`, [ ] ], then reverse of [ `[4, 7]`, reverse of [ ] ] = [ `[4, 7]`, [ ] ] (Transitive Property of Equality)
7	result of appending `[4, 7]` to [ ] = [ `[4, 7]`, [ ] ]	if result of appending `[4, 7]` to [ ] = reverse of [ `[4, 7]`, reverse of [ ] ] and reverse of [ `[4, 7]`, reverse of [ ] ] = [ `[4, 7]`, [ ] ], then result of appending `[4, 7]` to [ ] = [ `[4, 7]`, [ ] ] (Transitive Property of Equality)

Please log in to add comments